Termination w.r.t. Q proof of TRS/currying/Ste92motivation.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(cons, app(fun, x)), app(app(map, fun), xs))
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(filter2, app(fun, x)), fun)
APP(app(app(app(filter2, false), fun), x), xs) → APP(filter, fun)
APP(h, app(h, x)) → APP(app(f, app(h, x)), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(filter2, app(fun, x)), fun), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(fun, x)), fun), x), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(cons, x), app(app(filter, fun), xs))
APP(app(app(app(filter2, true), fun), x), xs) → APP(filter, fun)
APP(h, app(h, x)) → APP(f, app(h, x))
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(filter2, app(fun, x))
APP(app(app(app(filter2, true), fun), x), xs) → APP(cons, x)
APP(h, app(h, x)) → APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, x)) → APP(g, app(h, app(g, x)))
APP(g, app(g, x)) → APP(h, app(g, x))
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(cons, app(fun, x))

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(cons, app(fun, x)), app(app(map, fun), xs))
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(filter2, app(fun, x)), fun)
APP(app(app(app(filter2, false), fun), x), xs) → APP(filter, fun)
APP(h, app(h, x)) → APP(app(f, app(h, x)), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(filter2, app(fun, x)), fun), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(fun, x)), fun), x), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(cons, x), app(app(filter, fun), xs))
APP(app(app(app(filter2, true), fun), x), xs) → APP(filter, fun)
APP(h, app(h, x)) → APP(f, app(h, x))
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(filter2, app(fun, x))
APP(app(app(app(filter2, true), fun), x), xs) → APP(cons, x)
APP(h, app(h, x)) → APP(h, app(app(f, app(h, x)), x))
APP(g, app(g, x)) → APP(g, app(h, app(g, x)))
APP(g, app(g, x)) → APP(h, app(g, x))
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(cons, app(fun, x))

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(cons, app(fun, x)), app(app(map, fun), xs))
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(filter2, app(fun, x)), fun)
APP(h, app(h, x)) → APP(app(f, app(h, x)), x)
APP(app(app(app(filter2, false), fun), x), xs) → APP(filter, fun)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(filter2, app(fun, x)), fun), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(fun, x)), fun), x), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(cons, x), app(app(filter, fun), xs))
APP(app(app(app(filter2, true), fun), x), xs) → APP(filter, fun)
APP(h, app(h, x)) → APP(f, app(h, x))
APP(app(filter, fun), app(app(cons, x), xs)) → APP(filter2, app(fun, x))
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(h, app(h, x)) → APP(h, app(app(f, app(h, x)), x))
APP(app(app(app(filter2, true), fun), x), xs) → APP(cons, x)
APP(g, app(g, x)) → APP(h, app(g, x))
APP(g, app(g, x)) → APP(g, app(h, app(g, x)))
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(cons, app(fun, x))

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 14 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(g, app(g, x)) → APP(g, app(h, app(g, x)))

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

G1(G(x)) → G1(H(G(x)))

The TRS R consists of the following rules:

G(G(x)) → G(H(G(x)))
G(H(G(x))) → G(x)
H(H(x)) → H(f(H(x), x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP(g, app(g, x)) → APP(g, app(h, app(g, x)))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
G1(x1) = G1(x1)
G(x1) = G(x1)
H(x1) = H
f(x1, x2) = f(x1)

Recursive path order with status [2].
Quasi-Precedence:

G₁ > [G1₁, H]

Status:

G₁: multiset
H: multiset
f₁: multiset
G1₁: multiset

The following usable rules [14] were oriented:

app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)

The remaining pairs can at least be oriented weakly.

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)

Used ordering: Combined order from the following AFS and order.
APP(x1, x2) = x2
app(x1, x2) = app(x1, x2)
filter2 = filter2
true = true
filter = filter
map = map
cons = cons
false = false

Recursive path order with status [2].
Quasi-Precedence:

map > [app₂, filter2, cons, false]

Status:

filter: multiset
true: multiset
false: multiset
map: multiset
app₂: multiset
filter2: multiset
cons: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)

The TRS R consists of the following rules:

app(g, app(h, app(g, x))) → app(g, x)
app(g, app(g, x)) → app(g, app(h, app(g, x)))
app(h, app(h, x)) → app(h, app(app(f, app(h, x)), x))
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.